k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; tg.Type),
g:((tg:Id  (decl-state(ds)T(decl-type{i:l}(dt; tg) List))) List).
((isrcv(k))
 ((destination(lnk(k)) = source(l)  Id)
  ((eq_lnk(lnk(k); l))  (T = decl-type{i:l}(dt; tag(k))))))
 normal-ds{i:l}
 normal-ds(ds)
 normal-type{i:l}
 normal-type(T)
 normal-ds{i:l}
 normal-ds(dt)
 R-realizes{i:l}
 R-realizes(Rsends(ds; k; T; l; dt; g); es.sends-p(es; ds; k; T; l; dt; g)) 

latex

Definitions	x. t(x), prop{i:l}, t  T, A c B, R-Feasible{i:l}(R), R-realizes{i:l}(R; es.P(es)), P  Q, P  Q, x:A. B(x), x(s), R-consistent(R; es), normal-type{i:l}(T), normal-ds{i:l}(ds), decl-type{i:l}(ds; x)
Lemmas	Knd wf, IdLnk wf, fpf wf, decl-state wf, tagof wf, decl-type wf, lsrc wf, ldst wf, Id wf, isrcv wf, normal-type wf, normal-ds wf, event system wf, Rsends wf, R-consistent wf, lnk wf, eq lnk wf, assert wf